﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\Oracles\NFMs\Oracle_MAT_Realistic.cs
 * Description  :     A realistic oracle for deterministic Mealy machine for passive systems
 * Change log   :     -16 Feb 2013:  Initial version (by simplifying Oracle_NMAT_Realistic_Passive
 * To Do        :     -** Write the EQ part (the test case generation here is different!)
 *                    -There are lots of shared things with non-passive. we should not 
 * 					  repeate the same thing two times!
 * 					  - Unify test case execution and falsifier!
 ************************************************************************/
using System;
using System.Collections.Generic;
using AIDE.Base;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using MBT.Conformance.OfflineTesting;
using MBT.Conformance.OnlineTesting;
using MBT.Conformance.TestExecution;

namespace AIDE.Oracles.NFMs
{
	/// <summary>
	/// The real oracle which doesn't know the machine. 
	/// It has communication with SUL (in fact, an emulator of SUL)    
	/// </summary>
	public class Oracle_MAT_Realistic: IOracle_MAT_MM
	{
		//TODO: remove these stuff and use the 
		public int numberOfMQ, numberOfEQ;
		public TimeSpan EqTime = TimeSpan.Zero, OqTime = TimeSpan.Zero;
		DateTime startTime;
		IBlackBox_MM SUL;
		int Debugging_Level;

		/// <summary>
		/// Oracle for deterministic Mealy Machine
		/// </summary>
		/// <param name="SUT">the target Mealy Machine</param>
		public Oracle_MAT_Realistic (IBlackBox_MM SUT)
		{
			#region[Read config]
			if (!LibSetting.IsInitialized) {
				Console.Write ("Warning: The MTB configuration is not initialized! Initializing it...");
				LibSetting.Init ();
				Console.WriteLine ("Done!");
				//throw new Exception("Error: The MBT configuration is not initialized!");
			}
			if (!int.TryParse (LibSetting.ConfOf ("AIDE.Debugging_Level"), out Debugging_Level)) {
				Debugging_Level = 3;
			}
			typeOfTesting = int.Parse (LibSetting.ConfOf ("Testing.Algorithm"));
			//Console.WriteLine ("Testing approach: " + typeOfTesting);
			#endregion

			this.SUL = SUT;
			numberOfEQ = 0;
			numberOfMQ = 0;
		}

		public Alphabet InputAlphabet {
			get {
				return SUL.InputAlphabet;
			}
		}

		#region IOracle_MAT_MM Members
		IOracleLogHelper logHelper;

		public void SetLogger (IOracleLogHelper logHelper)
		{
			this.logHelper = logHelper;
		}

		/// <summary>
		/// Try to find a shourter counter example
		/// </summary>
		/// <param name="l">a founded counterexample</param>
		/// <returns></returns>
		Word ShortenCounterExample (Word l)
		{
			throw new NotImplementedException ();
		}

		/// <summary>
		/// Membership query: ask what is the output resulting from an input
		/// </summary>
		/// <param name="subwords">the subwords of a word to be examined</param>
		/// <returns>the resulting output</returns>
		public Word OutputTrace (params Word[] subwords)
		{
			if (logHelper != null)
				logHelper.BeforMembQuery ();

			numberOfMQ++;
			startTime = DateTime.Now;

			//* Make the input
			List < ISymbol > input = new List < ISymbol > ();
			for (int i = 0; i < subwords.Length; i++) {
				for (int j = 0; j < subwords[i].Length; j++)
					input.Add (subwords [i].GetSymByIndex (j));
			}

			LearningLog.LogStartSULReset ();
			SUL.Reset ();
			//Console.Write("\nQuery:");
			//Utils.ListUtil.WriteList (input);
			//Console.Write("\n");

			LearningLog.LogFinishSULReset ();

			//* Ask the system
			List < ISymbol > output = new List < ISymbol > ();
			for (int i = 0; i < input.Count; i++) {
				ISymbol o = SUL.Step (input [i]);

				//* to support input-incompletness!
				if (o == null) {
					if (logHelper != null)
						logHelper.AfterMemberQuery ();

					OqTime += (DateTime.Now - startTime);
					return null;
				}

				output.Add (o);
			}

			Word myWord = new Word ();
			for (int i = 0; i < output.Count; i++)
				myWord.AddSymbol (output [i]);

			OqTime += (DateTime.Now - startTime);

			if (logHelper != null)
				logHelper.AfterMemberQuery ();
			return myWord;
		}

		int typeOfTesting;

		/// <summary>
		///  See if a conjecture is equal to a black box or not. If they are not equal, find a counterexample to show the difference
		/// </summary>
		/// <param name="conjucture">the conjecture to be compared with DFA</param>
		/// <returns>null if they are equal, a distinguishing counterexample if not</returns>
		public Word EquivalenceQ (MealyMachine conjucture)
		{
			if (logHelper != null) {
				logHelper.BeforEquivQuery ();
			}

			startTime = DateTime.Now;
			numberOfEQ++;
			//typeOfTesting = 3;
			if (typeOfTesting == 0) {
				Console.WriteLine ("Conformance Testing (Edge Coverage)!");
				//* 1: Test case generator- Policy: Edge Coverag
				OTCG_EdgeCoverage < MealyMachine.Mealy_State, MealyMachine.Mealy_Transition > ec = new OTCG_EdgeCoverage < MealyMachine.Mealy_State, MealyMachine.Mealy_Transition > (conjucture, null);

				ec.GenerateTestCases ();
				//* 2- Test case executor
				MealyTCE te = new MealyTCE (SUL, true);
				te.SetModel (conjucture);


				foreach (List < MealyMachine.Mealy_Transition > tc in ec.EnumerateTestCases()) {
					List < PairOfSymbols > counterexample = null;
					try {
						counterexample = (List < PairOfSymbols >)te.FalsifyTestCase (tc);
					} catch {
						Console.WriteLine ("Error!");
					}

					if (counterexample != null) {
						Word ce = new Word ();
						for (int i = 0; i < counterexample.Count; i++)
							ce.AddSymbol (counterexample [i].Input);

						if (logHelper != null) {
							logHelper.FoundCounterExample ();
							logHelper.AfterEquivQuery ();
						}
						return ce;
					}
				}
			} else if (typeOfTesting == 1) {
				Console.WriteLine ("Conformance Testing (W-Method)!");
				OTCG_WMethod < MealyMachine.Mealy_State, MealyMachine.Mealy_Transition > tcgW = new OTCG_WMethod < MealyMachine.Mealy_State, MealyMachine.Mealy_Transition > (conjucture);

				//OTCG_WpMethod<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition> tcgW1 = 
				//		new OTCG_WpMethod<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition>(conjucture);
				//OTCG_WMethod<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition> tcgW = 
				//		new OTCG_WMethod<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition>(conjucture);
				tcgW.Process ();
				List < Word > ts = tcgW.GenerateTestSuite ();
				Console.WriteLine ("Number of tests: " + ts.Count);
				//return null;

				foreach (Word tc in ts) {
					Console.WriteLine (tc);
					//continue;

					bool res = ExecuteTestCase (conjucture, tc);
					if (!res) {
						Console.WriteLine ("Counterexample!");

						if (logHelper != null) {
							logHelper.FoundCounterExample ();
							logHelper.AfterEquivQuery ();
						}
						return tc;
					}
				}
			} else if (typeOfTesting == 2) {
				OTCG_PathCoverage < MealyMachine.Mealy_State, MealyMachine.Mealy_Transition > tcgP = new OTCG_PathCoverage < MealyMachine.Mealy_State, MealyMachine.Mealy_Transition > (conjucture);

				//* 2- Test case executor
				MealyTCE te = new MealyTCE (SUL, true);
				te.SetModel (conjucture);

				foreach (List < MealyMachine.Mealy_Transition > tc in tcgP.EnumerateTestCases()) {
					AIDE.Utils.ListUtil.WriteList (tc, ",");
					Console.WriteLine ();
					List < PairOfSymbols > counterexample = null;
					try {
						counterexample = (List < PairOfSymbols >)te.FalsifyTestCase (tc);
					} catch {
						Console.WriteLine ("Error!");
					}

					if (counterexample != null) {
						Word ce = new Word ();
						for (int i = 0; i < counterexample.Count; i++)
							ce.AddSymbol (counterexample [i].Input);
						if (logHelper != null) {
							logHelper.FoundCounterExample ();
							logHelper.AfterEquivQuery ();
						}
						return ce;
					}
				}
			} else if (typeOfTesting == 3) {
				Onlt_RandomWalk_FSM tcgP = new Onlt_RandomWalk_FSM (conjucture);
				//Console.WriteLine("Conformance Testing (Random Walk)!");
				string NumberOfCesStr = LibSetting.ConfOf ("Testing.NumberOfCEs");
				int NumberOfCEs;
				if (NumberOfCesStr != null && NumberOfCesStr.Length > 0)
					NumberOfCEs = int.Parse (NumberOfCesStr);
				else
					NumberOfCEs = 1;
				List<Word> cexs = new List<Word> ();

				//* 2- Test case executor
				MealyTCE te = new MealyTCE (SUL, true);
				te.SetModel (conjucture);
				int testNum = 0;
				foreach (List < MealyMachine.Mealy_Transition > tc in tcgP.EnumerateTestCases()) {
					if (Debugging_Level >= 3)
						Console.Write ("\n" + testNum + ".");
					testNum++;
					if (Debugging_Level >= 3) {
						AIDE.Utils.ListUtil.WriteList (tc, ",");
						Console.WriteLine ();
					}
					List < PairOfSymbols > counterexample = null;

					counterexample = (List < PairOfSymbols >)te.FalsifyTestCase (tc);
					/*
					try {
						//LearningLog.LogStartStepOnSUL();
						//* this function will run only 1 experiment on SUL [the system is deterministic]
						counterexample = (List < PairOfSymbols >)te.FalsifyTestCase (tc);
						//LearningLog.LogFinishStepOnSUL();
					} catch {
						Console.WriteLine ("Error in testing!");
					}*/

					if (counterexample != null) {
						Word ce = new Word ();
						for (int i = 0; i < counterexample.Count; i++)
							ce.AddSymbol (counterexample [i].Input);

						if (logHelper != null) {
							//* log the counterexample
							logHelper.FoundCounterExample ();
							logHelper.AfterEquivQuery ();
						}
						cexs.Add (ce);
						if (cexs.Count >= NumberOfCEs)
							break;
						//return ce;
					}
				}

				if (cexs.Count != 0) {
					int min = int.MaxValue, minIndex = -1;
					for (int i=0; i<cexs.Count; i++) {
						if (Debugging_Level >= 3)
							Console.WriteLine (cexs [i].Length + ",");
						if (cexs [i].Length < min) {
							min = cexs [i].Length;
							minIndex = i;
						}
					}
					//Console.WriteLine ("Number of found counterexample: " + cexs.Count);
					Console.WriteLine ("Counterexample["+cexs.Count+"]: "+ cexs [minIndex]);
					return cexs [minIndex];
				}

			}
			if (logHelper != null) {
				logHelper.AfterEquivQuery ();
			}
			return null;
		}
		//TODO: use the "general" text case execution
		bool ExecuteTestCase (MealyMachine conj, Word path)
		{
			//TestResultType testResult = TestResultType.NoError;
			//DateTime temp = DateTime.Now;
			LearningLog.LogStartSULReset ();
			SUL.Reset ();
			LearningLog.LogFinishSULReset ();
			MealyMachine.Mealy_State currNode = (MealyMachine.Mealy_State)conj [0];
			for (int i = 0; i < path.Length; i++) {
				//string inp = path[i].edgeLabel.Substring(0, path[i].edgeLabel.IndexOf("/"));
				//string cop = path[i].edgeLabel.Substring(path[i].edgeLabel.IndexOf("/") + 1,
				//path[i].edgeLabel.Length - path[i].edgeLabel.IndexOf("/") - 1);

				LearningLog.LogStartStepOnSUL ();
				ISymbol outputSymb = SUL.Step (path [i]);
				LearningLog.LogFinishStepOnSUL ();

				if (outputSymb == null) {
					//testResult = TestResultType.PathNotReached;
					return false;
				}
				ISymbol output;
				currNode = currNode.NextNode (path [i], out output);

				if (output.Equals (outputSymb))
					continue;
				else {
					//testResult = TestResultType.NotAcceptedOutput;
					return false;
				}
			}
			//testResult = TestResultType.Passed;
			return true;
		}
		#endregion
	}
}